concat(leaf, Y) → Y
concat(cons(U, V), Y) → cons(U, concat(V, Y))
lessleaves(X, leaf) → false
lessleaves(leaf, cons(W, Z)) → true
lessleaves(cons(U, V), cons(W, Z)) → lessleaves(concat(U, V), concat(W, Z))
↳ QTRS
↳ DependencyPairsProof
concat(leaf, Y) → Y
concat(cons(U, V), Y) → cons(U, concat(V, Y))
lessleaves(X, leaf) → false
lessleaves(leaf, cons(W, Z)) → true
lessleaves(cons(U, V), cons(W, Z)) → lessleaves(concat(U, V), concat(W, Z))
CONCAT(cons(U, V), Y) → CONCAT(V, Y)
LESSLEAVES(cons(U, V), cons(W, Z)) → CONCAT(W, Z)
LESSLEAVES(cons(U, V), cons(W, Z)) → CONCAT(U, V)
LESSLEAVES(cons(U, V), cons(W, Z)) → LESSLEAVES(concat(U, V), concat(W, Z))
concat(leaf, Y) → Y
concat(cons(U, V), Y) → cons(U, concat(V, Y))
lessleaves(X, leaf) → false
lessleaves(leaf, cons(W, Z)) → true
lessleaves(cons(U, V), cons(W, Z)) → lessleaves(concat(U, V), concat(W, Z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
CONCAT(cons(U, V), Y) → CONCAT(V, Y)
LESSLEAVES(cons(U, V), cons(W, Z)) → CONCAT(W, Z)
LESSLEAVES(cons(U, V), cons(W, Z)) → CONCAT(U, V)
LESSLEAVES(cons(U, V), cons(W, Z)) → LESSLEAVES(concat(U, V), concat(W, Z))
concat(leaf, Y) → Y
concat(cons(U, V), Y) → cons(U, concat(V, Y))
lessleaves(X, leaf) → false
lessleaves(leaf, cons(W, Z)) → true
lessleaves(cons(U, V), cons(W, Z)) → lessleaves(concat(U, V), concat(W, Z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
CONCAT(cons(U, V), Y) → CONCAT(V, Y)
concat(leaf, Y) → Y
concat(cons(U, V), Y) → cons(U, concat(V, Y))
lessleaves(X, leaf) → false
lessleaves(leaf, cons(W, Z)) → true
lessleaves(cons(U, V), cons(W, Z)) → lessleaves(concat(U, V), concat(W, Z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
CONCAT(cons(U, V), Y) → CONCAT(V, Y)
The value of delta used in the strict ordering is 1.
POL(cons(x1, x2)) = 1/4 + (4)x_2
POL(CONCAT(x1, x2)) = (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
concat(leaf, Y) → Y
concat(cons(U, V), Y) → cons(U, concat(V, Y))
lessleaves(X, leaf) → false
lessleaves(leaf, cons(W, Z)) → true
lessleaves(cons(U, V), cons(W, Z)) → lessleaves(concat(U, V), concat(W, Z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
LESSLEAVES(cons(U, V), cons(W, Z)) → LESSLEAVES(concat(U, V), concat(W, Z))
concat(leaf, Y) → Y
concat(cons(U, V), Y) → cons(U, concat(V, Y))
lessleaves(X, leaf) → false
lessleaves(leaf, cons(W, Z)) → true
lessleaves(cons(U, V), cons(W, Z)) → lessleaves(concat(U, V), concat(W, Z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
LESSLEAVES(cons(U, V), cons(W, Z)) → LESSLEAVES(concat(U, V), concat(W, Z))
The value of delta used in the strict ordering is 1/16.
POL(cons(x1, x2)) = 1/4 + x_1 + x_2
POL(LESSLEAVES(x1, x2)) = (1/4)x_2
POL(concat(x1, x2)) = x_1 + x_2
POL(leaf) = 0
concat(leaf, Y) → Y
concat(cons(U, V), Y) → cons(U, concat(V, Y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
concat(leaf, Y) → Y
concat(cons(U, V), Y) → cons(U, concat(V, Y))
lessleaves(X, leaf) → false
lessleaves(leaf, cons(W, Z)) → true
lessleaves(cons(U, V), cons(W, Z)) → lessleaves(concat(U, V), concat(W, Z))